E,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), e:E. rcv?(e)   

latex

Definitions	x:A. B(x), t  T, rcv?(e), x. t(x), x,y. t(x;y), x(s), x(s1,s2)
Lemmas	ecase1 wf, bool wf, bfalse wf, Id wf, btrue wf, IdLnk wf